$\forall$$R$:es\_realizer\{i:l\}, $P$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$). $R$ $\Vdash$\{i\} ${\it es}$.$P$(${\it es}$) $\in$ Prop$_{\mbox{\scriptsize i''}}$